Left Termination of the query pattern
prime(g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToPiTRSProof (⇒, 74 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 208 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 PiDP
        ↳36 UsableRulesProof (⇔, 0 ms)
        ↳37 PiDP
        ↳38 PiDPToQDPProof (⇒, 0 ms)
        ↳39 QDP
        ↳40 QDPOrderProof (⇔, 122 ms)
        ↳41 QDP
        ↳42 DependencyGraphProof (⇔, 0 ms)
        ↳43 TRUE

(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).
prime(s(s(X))) :- pr(s(s(X)), s(X)).
pr(X, s(0)).
pr(X, s(s(Y))) :- ','(not_divides(s(s(Y)), X), pr(X, s(Y))).
not_divides(Y, X) :- ','(div(X, Y, U), ','(times(U, Y, Z), neq(X, Z))).
neq(s(X), 0).
neq(0, s(X)).
neq(s(X), s(Y)) :- neq(X, Y).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(times(X, Y, U), add(U, Y, Z)).
add(X, 0, X).
add(0, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).

Query: prime(g)

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
prime_in: (b)
pr_in: (b,b)
not_divides_in: (b,b)
div_in: (b,b,f)
quot_in: (b,b,b,f)
times_in: (b,b,f)
add_in: (b,b,f)
neq_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PRIME_IN_G(s(s(X))) → U4_G(X, pr_in_gg(s(s(X)), s(X)))
PRIME_IN_G(s(s(X))) → PR_IN_GG(s(s(X)), s(X))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
PR_IN_GG(X, s(s(Y))) → NOT_DIVIDES_IN_GG(s(s(Y)), X)
NOT_DIVIDES_IN_GG(Y, X) → U7_GG(Y, X, div_in_gga(X, Y, U))
NOT_DIVIDES_IN_GG(Y, X) → DIV_IN_GGA(X, Y, U)
DIV_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
DIV_IN_GGA(X, Y, Z) → QUOT_IN_GGGA(X, Y, Y, Z)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → U2_GGGA(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → U3_GGGA(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
U7_GG(Y, X, div_out_gga(X, Y, U)) → U8_GG(Y, X, times_in_gga(U, Y, Z))
U7_GG(Y, X, div_out_gga(X, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U11_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U12_GGA(X, Y, Z, add_in_gga(U, Y, Z))
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → ADD_IN_GGA(U, Y, Z)
ADD_IN_GGA(s(X), Y, s(Z)) → U13_GGA(X, Y, Z, add_in_gga(X, Y, Z))
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
U8_GG(Y, X, times_out_gga(U, Y, Z)) → U9_GG(Y, X, neq_in_gg(X, Z))
U8_GG(Y, X, times_out_gga(U, Y, Z)) → NEQ_IN_GG(X, Z)
NEQ_IN_GG(s(X), s(Y)) → U10_GG(X, Y, neq_in_gg(X, Y))
NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_GG(X, Y, pr_in_gg(X, s(Y)))
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
PRIME_IN_G(x1)  =  PRIME_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x2)
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
NOT_DIVIDES_IN_GG(x1, x2)  =  NOT_DIVIDES_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
DIV_IN_GGA(x1, x2, x3)  =  DIV_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x4)
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x5)
U3_GGGA(x1, x2, x3, x4)  =  U3_GGGA(x4)
U8_GG(x1, x2, x3)  =  U8_GG(x2, x3)
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
NEQ_IN_GG(x1, x2)  =  NEQ_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U6_GG(x1, x2, x3)  =  U6_GG(x3)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PRIME_IN_G(s(s(X))) → U4_G(X, pr_in_gg(s(s(X)), s(X)))
PRIME_IN_G(s(s(X))) → PR_IN_GG(s(s(X)), s(X))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
PR_IN_GG(X, s(s(Y))) → NOT_DIVIDES_IN_GG(s(s(Y)), X)
NOT_DIVIDES_IN_GG(Y, X) → U7_GG(Y, X, div_in_gga(X, Y, U))
NOT_DIVIDES_IN_GG(Y, X) → DIV_IN_GGA(X, Y, U)
DIV_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
DIV_IN_GGA(X, Y, Z) → QUOT_IN_GGGA(X, Y, Y, Z)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → U2_GGGA(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → U3_GGGA(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
U7_GG(Y, X, div_out_gga(X, Y, U)) → U8_GG(Y, X, times_in_gga(U, Y, Z))
U7_GG(Y, X, div_out_gga(X, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U11_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U12_GGA(X, Y, Z, add_in_gga(U, Y, Z))
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → ADD_IN_GGA(U, Y, Z)
ADD_IN_GGA(s(X), Y, s(Z)) → U13_GGA(X, Y, Z, add_in_gga(X, Y, Z))
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
U8_GG(Y, X, times_out_gga(U, Y, Z)) → U9_GG(Y, X, neq_in_gg(X, Z))
U8_GG(Y, X, times_out_gga(U, Y, Z)) → NEQ_IN_GG(X, Z)
NEQ_IN_GG(s(X), s(Y)) → U10_GG(X, Y, neq_in_gg(X, Y))
NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_GG(X, Y, pr_in_gg(X, s(Y)))
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
PRIME_IN_G(x1)  =  PRIME_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x2)
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
NOT_DIVIDES_IN_GG(x1, x2)  =  NOT_DIVIDES_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
DIV_IN_GGA(x1, x2, x3)  =  DIV_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x4)
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x5)
U3_GGGA(x1, x2, x3, x4)  =  U3_GGGA(x4)
U8_GG(x1, x2, x3)  =  U8_GG(x2, x3)
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
NEQ_IN_GG(x1, x2)  =  NEQ_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U6_GG(x1, x2, x3)  =  U6_GG(x3)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 19 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
NEQ_IN_GG(x1, x2)  =  NEQ_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(s(X), Y) → ADD_IN_GGA(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADD_IN_GGA(s(X), Y) → ADD_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 >= 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT_IN_GGGA(X, 0, s(Z)) → QUOT_IN_GGGA(X, s(Z), s(Z))
QUOT_IN_GGGA(s(X), s(Y), Z) → QUOT_IN_GGGA(X, Y, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • QUOT_IN_GGGA(s(X), s(Y), Z) → QUOT_IN_GGGA(X, Y, Z)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOT_IN_GGGA(X, 0, s(Z)) → QUOT_IN_GGGA(X, s(Z), s(Z))
    The graph contains the following edges 1 >= 1, 3 >= 2, 3 >= 3

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))

The TRS R consists of the following rules:

not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_GG(X, Y, not_divides_out_gg) → PR_IN_GG(X, s(Y))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))

The TRS R consists of the following rules:

not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y))
U7_gg(Y, X, div_out_gga(U)) → U8_gg(X, times_in_gga(U, Y))
div_in_gga(X, Y) → U1_gga(quot_in_ggga(X, Y, Y))
U8_gg(X, times_out_gga(Z)) → U9_gg(neq_in_gg(X, Z))
U1_gga(quot_out_ggga(Z)) → div_out_gga(Z)
times_in_gga(0, Y) → times_out_gga(0)
times_in_gga(s(X), Y) → U11_gga(Y, times_in_gga(X, Y))
U9_gg(neq_out_gg) → not_divides_out_gg
quot_in_ggga(0, s(Y), s(Z)) → quot_out_ggga(0)
quot_in_ggga(s(X), s(Y), Z) → U2_ggga(quot_in_ggga(X, Y, Z))
quot_in_ggga(X, 0, s(Z)) → U3_ggga(quot_in_ggga(X, s(Z), s(Z)))
U11_gga(Y, times_out_gga(U)) → U12_gga(add_in_gga(U, Y))
neq_in_gg(s(X), 0) → neq_out_gg
neq_in_gg(0, s(X)) → neq_out_gg
neq_in_gg(s(X), s(Y)) → U10_gg(neq_in_gg(X, Y))
U2_ggga(quot_out_ggga(U)) → quot_out_ggga(U)
U3_ggga(quot_out_ggga(U)) → quot_out_ggga(s(U))
U12_gga(add_out_gga(Z)) → times_out_gga(Z)
U10_gg(neq_out_gg) → neq_out_gg
add_in_gga(X, 0) → add_out_gga(X)
add_in_gga(0, X) → add_out_gga(X)
add_in_gga(s(X), Y) → U13_gga(add_in_gga(X, Y))
U13_gga(add_out_gga(Z)) → add_out_gga(s(Z))

The set Q consists of the following terms:

not_divides_in_gg(x0, x1)
U7_gg(x0, x1, x2)
div_in_gga(x0, x1)
U8_gg(x0, x1)
U1_gga(x0)
times_in_gga(x0, x1)
U9_gg(x0)
quot_in_ggga(x0, x1, x2)
U11_gga(x0, x1)
neq_in_gg(x0, x1)
U2_ggga(x0)
U3_ggga(x0)
U12_gga(x0)
U10_gg(x0)
add_in_gga(x0, x1)
U13_gga(x0)

We have to consider all (P,Q,R)-chains.

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(PR_IN_GG(x1, x2)) = x2   
POL(U10_gg(x1)) = 0   
POL(U11_gga(x1, x2)) = 0   
POL(U12_gga(x1)) = 0   
POL(U13_gga(x1)) = 0   
POL(U1_gga(x1)) = 0   
POL(U2_ggga(x1)) = 0   
POL(U3_ggga(x1)) = 0   
POL(U5_GG(x1, x2, x3)) = 1 + x2   
POL(U7_gg(x1, x2, x3)) = 0   
POL(U8_gg(x1, x2)) = 0   
POL(U9_gg(x1)) = 0   
POL(add_in_gga(x1, x2)) = 0   
POL(add_out_gga(x1)) = 0   
POL(div_in_gga(x1, x2)) = 0   
POL(div_out_gga(x1)) = 0   
POL(neq_in_gg(x1, x2)) = 0   
POL(neq_out_gg) = 0   
POL(not_divides_in_gg(x1, x2)) = 0   
POL(not_divides_out_gg) = 0   
POL(quot_in_ggga(x1, x2, x3)) = 1 + x1 + x3   
POL(quot_out_ggga(x1)) = 0   
POL(s(x1)) = 1 + x1   
POL(times_in_gga(x1, x2)) = 0   
POL(times_out_gga(x1)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_GG(X, Y, not_divides_out_gg) → PR_IN_GG(X, s(Y))

The TRS R consists of the following rules:

not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y))
U7_gg(Y, X, div_out_gga(U)) → U8_gg(X, times_in_gga(U, Y))
div_in_gga(X, Y) → U1_gga(quot_in_ggga(X, Y, Y))
U8_gg(X, times_out_gga(Z)) → U9_gg(neq_in_gg(X, Z))
U1_gga(quot_out_ggga(Z)) → div_out_gga(Z)
times_in_gga(0, Y) → times_out_gga(0)
times_in_gga(s(X), Y) → U11_gga(Y, times_in_gga(X, Y))
U9_gg(neq_out_gg) → not_divides_out_gg
quot_in_ggga(0, s(Y), s(Z)) → quot_out_ggga(0)
quot_in_ggga(s(X), s(Y), Z) → U2_ggga(quot_in_ggga(X, Y, Z))
quot_in_ggga(X, 0, s(Z)) → U3_ggga(quot_in_ggga(X, s(Z), s(Z)))
U11_gga(Y, times_out_gga(U)) → U12_gga(add_in_gga(U, Y))
neq_in_gg(s(X), 0) → neq_out_gg
neq_in_gg(0, s(X)) → neq_out_gg
neq_in_gg(s(X), s(Y)) → U10_gg(neq_in_gg(X, Y))
U2_ggga(quot_out_ggga(U)) → quot_out_ggga(U)
U3_ggga(quot_out_ggga(U)) → quot_out_ggga(s(U))
U12_gga(add_out_gga(Z)) → times_out_gga(Z)
U10_gg(neq_out_gg) → neq_out_gg
add_in_gga(X, 0) → add_out_gga(X)
add_in_gga(0, X) → add_out_gga(X)
add_in_gga(s(X), Y) → U13_gga(add_in_gga(X, Y))
U13_gga(add_out_gga(Z)) → add_out_gga(s(Z))

The set Q consists of the following terms:

not_divides_in_gg(x0, x1)
U7_gg(x0, x1, x2)
div_in_gga(x0, x1)
U8_gg(x0, x1)
U1_gga(x0)
times_in_gga(x0, x1)
U9_gg(x0)
quot_in_ggga(x0, x1, x2)
U11_gga(x0, x1)
neq_in_gg(x0, x1)
U2_ggga(x0)
U3_ggga(x0)
U12_gga(x0)
U10_gg(x0)
add_in_gga(x0, x1)
U13_gga(x0)

We have to consider all (P,Q,R)-chains.

(42) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(43) TRUE